\begin{tabbing}
$\forall$$A$, $B$:Type, $f_{0}$:$A$, $g_{0}$:$B$, $F$:($\mathbb{N}\rightarrow$$A$$\rightarrow$$B$$\rightarrow$$A$), $G$:($\mathbb{N}\rightarrow$$A$$\rightarrow$$B$$\rightarrow$$B$).
\\[0ex]$\exists$\=$f$:$\mathbb{N}\rightarrow$$A$\+
\\[0ex]$\exists$\=$g$:$\mathbb{N}\rightarrow$$B$\+
\\[0ex]($f$(0) = $f_{0}$
\\[0ex]\& $g$(0) = $g_{0}$
\\[0ex]\& ($\forall$$s$:$\mathbb{N}^{+}$. $f$($s$) = $F$($s$ {-} 1,$f$($s$ {-} 1),$g$($s$ {-} 1)) \& $g$($s$) = $G$($s$ {-} 1,$f$($s$ {-} 1),$g$($s$ {-} 1))))
\-\-
\end{tabbing}